nLab homotopy type with finite homotopy groups

Idea

The concept of a homotopy type (homotopy n-type) all of whose homotopy groups are finite groups does not have an established name. Sometimes it is called $\pi$-finiteness. In the context of groupoid cardinality “tameness” is used. In homological algebra “of finite type” is used, which in homotopy theory however badly clashes with the concept of finite homotopy type which is crucially different from homotopy type with finite homotopy groups. (Anel 21) uses “truncated coherent spaces”.

Properties

(Co-)Limits indexed by homotopy types with finite homotopy groups

see at K(n)-local stable homotopy theory (…)

Relation to coherent objects

Proposition

∞Grpd is a coherent (∞,1)-topos and a locally coherent (∞,1)-topos. An object $X$, hence an ∞-groupoid, is an n-coherent object precisely if all its homotopy groups in degree $k \leq n$ are finite. Hence the fully coherent objects here are the homotopy types with finite homotopy groups.

(Lurie SpecSchm, example 3.13)

Proposition

The $(\infty, 1)$-category of homotopy types with finite homotopy groups is the initial (∞,1)-pretopos.

(Anel 21, Theorem 2.6.6).

Codensity monad of the inclusion into all homotopy types

The inclusion of homotopy types with finite groups into all homotopy types generates a codensity monad whose algebras lie somewhere between totally disconnected compact Hausdorff condensed $\infty$-groupoids, and all compact Hausdorff condensed $\infty$-groupoids. (See Scholze for more details.)

Related concepts

• finite homotopy type

• finite type

• pi-finite type

References

• G. J. Ellis, Spaces with finitely many non-trivial homotopy groups all of which are finite, Topology, 36, (1997), 501–504, ISSN 0040-9383.

• Jean-Louis Loday, Spaces with finitely many non-trivial homotopy groups (pdf)

• Peter Scholze, Infinity-categorical analogue of compact Hausdorff, MO answer

Discussion as an elementary (∞,1)-topos:

• Mathieu Anel, The elementary infinity-topos of truncated coherent spaces (arXiv:2107.02082)

Formalization in homotopy type theory (via Agda):

• UniMath project, π-finite types [web]